COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	properties of allp
C00003 00003	proofs allp
C00005 ENDMK
C⊗;
;properties of allp
(wipe-out)
(get-proofs lispax)

(proof allp)
;the following formulation of the definition of allp is more convenient when
;deriving instead of rewriting

(axiom |∀phi x u.allp(phi,x.u)⊃phi(x)∧allp(phi,u)|)
(label allpfact)

(axiom |∀phi1 u.(∀y.member(y,u)⊃phi1(y))⊃allp(phi1,u)|)
(label allp_introduction)

(axiom |∀phi1 x u.member(x,u)∧allp(phi1,u)⊃phi1(x)|)
(label allp_elimination)

(axiom |∀u a a1.allp(a,u)∧(∀x.a(x)⊃a1(x))⊃allp(a1,u)|)
(label allp_implication)
(save-proofs allp)
;proofs allp

(proof allpprop)

;allpfact

(trw |∀phi x u.allp(phi,x.u)⊃phi(x)∧allp(phi,u)| (open allp))
;∀PHI X U.ALLP(PHI,X.U)⊃PHI(X)∧ALLP(PHI,U)

;allp_introduction

(ue (phi |λu.(∀y.member(y,u)⊃phi1(y))⊃allp(phi1,u)|)
    listinduction (open allp member) (use normal mode: always))
;∀U.(∀Y.MEMBER(Y,U)⊃PHI1(Y))⊃ALLP(PHI1,U)

;allp_elimination

(ue (phi |λu.member(x,u)∧allp(phi1,u)⊃phi1(x)|) listinduction 
    (part 1 (open member allp) (use normal mode: always)))
;∀U.MEMBER(X,U)∧ALLP(PHI1,U)⊃PHI1(X)

;allp_implication

(ue (phi |λu.∀a a1.allp(a,u)∧(∀x.a(x)⊃a1(x))⊃allp(a1,u)|) listinduction 
    (open allp))
;∀U A A1.ALLP(A,U)∧(∀X.A(X)⊃A1(X))⊃ALLP(A1,U)